This invention relates generally to formal verification of circuit designs, and more particularly to constraining of traces found in formal verification.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation, and formal verification. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among the combinational logic between registers.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical tools to create a HDL-based design.
An increasingly popular technique is to use formal methods to verify the properties of a design completely. Formal methods use mathematical techniques to prove that a design property is either always true or to provide an example condition (called a counterexample) that demonstrates the property is false. Tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include specifications and/or requirements that must be satisfied by the circuit design. The formal verification technology requires that the requirements are expressed in a formal notation, for example a temporal language, which enables an exhaustive mathematical check for whether a design complies with the requirements.
Although a counterexample demonstrates an example condition under which a circuit design fails a property, the cause of the failure is not always obvious. Accordingly, what are needed are techniques to view and analyze the results of formal verification of a circuit design (such as a counterexample) to help circuit designers understand the results obtained from the formal verification (e.g., why a particular property failed).